1. Field of the Invention
Embodiments of the invention generally relate to electronic design automation and, more specifically, to a method and apparatus for processing assertions in assertion-based verification of a logic design.
2. Description of the Related Art
In electronic design automation (EDA), functional verification is the task of verifying that a logic design conforms to its specification. Logic simulation is the process of simulating a logic design before the logic design manufactured as integrated circuits (ICs). Logic designs may be described using various languages, such as hardware description languages (HDLs) or other more abstract languages (e.g., synthesizable SystemC). In simulation, engineers write a test-bench program to functionally verify the logic design by providing meaningful scenarios to check that, given certain input stimuli, the design performs to specification. A test-bench may be written using various languages, including lower-level languages, such as very high speed integrated circuit HDL (VHDL), Verilog, and the like, as well as more abstract languages, such as C/C++, SystemC, SystemVerilog, and the like.
In software simulation, a description of the logic design is simulated on computers or workstations. Pure software simulation, however, decreases in performance as the logic design becomes larger and more complex. Simulation acceleration addresses the performance shortcomings of pure software simulation. In simulation acceleration, the logic design is mapped into a hardware accelerator to provide a design under verification (DUV), which allows the design to run much faster than on a general-purpose computer or workstation. The test-bench continues to run using a software simulator on a computer or workstation. A communication channel connects the software simulator and the hardware accelerator to exchange data between the test-bench and design.
A recent design verification method, known as assertion-based verification, involves testing a simulation of the circuit against one or more assertions describing how the circuit should behave. An “assertion” is a statement that a certain property must be true, for example, that a first asserted signal must always be followed by a second asserted signal within two clock cycles. Assertions allow for automated checking that the specified property is true, and can generate automatic error messages if the property is not true. Industry organizations have defined standardized assertion languages that designers can use to specify their assertions.
Assertion languages often support two kinds of assertions: concurrent and immediate. Immediate assertions, sometimes also called combinational assertions, follow simulation event semantics for their execution and are executed like a statement in a procedural block. Concurrent assertions, on the other hand, are temporal in nature and are based on clock semantics and use time-sampled values of variables. Concurrent assertions are sometimes also called sequential assertions.
In a simulation verification environment, assertions are validated continuously during simulation to ensure expected design behavior. To prevent degradation of performance in a hardware-based accelerator system, it is as important to accelerate assertion checking as to accelerate the logic design being simulated. One known technique for assertion acceleration involves use of a static, synthesizable model that can represent any snapshot of simultaneously active assertion match attempts during simulation. Targeting the different possible scenarios of an assertion (i.e., the remaining criteria for a successful match), the technique constructs a deterministic finite automata (DFA) model, where each possible scenario of the assertion is explicitly encoded as a distinct state in the DFA.
The DFA technique has two fundamental drawbacks that limit its applicability. First, the DFA technique must explicitly encode all possible scenarios to capture any snapshot, including the one where all possible scenarios occur simultaneously even though it might not be the case in a particular simulation run. As a result, the numbers of DFA states and state transitions typically increase non-linearly and explode exponentially. Second, the DFA approach is a flattened snapshot solution. It can capture the scenarios of all ongoing match attempts, but cannot distinguish between different attempts that transition into the same DFA state. This coalescing of match attempts makes it unnatural for the DFA approach to maintain separate local environments for different attempts. As such, it is typically infeasible for the DFA approach to support “attempt-sensitive” controls as defined in some assertion languages, such as the System Verilog assertion language.
Accordingly, there exists a need in the art for an improved method and apparatus for processing assertions in assertion-based verification of a logic design.